<HEAD><TITLE>hindley-milner</TITLE>
<META http-equiv="Content-Style-Type" content="text/css" />
<META http-equiv="content-type" content="text/html; charset=utf-8" />  
<STYLE type="text/css">
 pre.code {
        margin: 15px;
       background-color: #FFFFFF;
       font-family: Mono, Fixed;
       font-weight: Normal;
       font-size: 14px;
}
span.Red1 {color: rgb(212,0,0);}
span.Red2 {color: rgb(253,51,1);}
span.Red3 {color: rgb(244,72,0);}
span.Blue1 {color: rgb(0,136,170);}
span.Blue2 {color: rgb(0,102,128);}
span.Blue3 {color: rgb(0,51,153);}
span.Purple1 {color: rgb(180,120,204);}
span.Purple2 {color: rgb(156,72,184);}
span.Purple3 {color: rgb(100,0,136);}
span.Yellow1 {color: rgb(240,236,4);}
span.Yellow2 {color: rgb(224,212,12);}
span.Yellow3 {color: rgb(184,160,28);}
span.Brown1 {color: rgb(238,199,62);}
span.Brown2 {color: rgb(204,102,51);}
span.Brown3 {color: rgb(152,102,1);}
span.Orange1 {color: rgb(255,102,51);}
span.Orange2 {color: rgb(255,153,51);}
span.Orange3 {color: rgb(255,204,0);}
span.Grey1 {color: rgb(153,153,153);}
span.Grey2 {color: rgb(128,128,128);}
span.Grey3 {color: rgb(102,102,102);}
span.Grey4 {color: rgb(51,51,51);}
span.Green1 {color: rgb(102,204,0);}
span.Green2 {color: rgb(102,204,102);}
span.Green3 {color: rgb(51,153,102);}
</STYLE>
</HEAD>

<BODY>
<PRE class="code"><SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Hindley-Milner Type Inference. http://ian-grant.net/hm </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3">datatype</SPAN></i> <SPAN class="Grey2">term</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN>
              <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">Tyapp</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">term</SPAN> <SPAN class="Grey2">list</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">subs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">term</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">term</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">ss</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">term</SPAN> <i><SPAN class="Yellow3">as</SPAN></i> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
       <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">v1</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">t1</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">ss</SPAN> <SPAN class="Grey2">term</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">term</SPAN> <i><SPAN class="Yellow3">as</SPAN></i> <SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">term</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">l</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
       <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Brown1">rev</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
             <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                   <SPAN class="Grey2">arglist</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">l</SPAN> <SPAN class="Grey2">h</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN>
       <i><SPAN class="Yellow3">in</SPAN></i>
          <SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
       <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">compose</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">s1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">s1</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">compose</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">ss</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">s1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
      <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Brown1">rev</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>  
            <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">ss</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                 <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Grey2">ss</SPAN>
      <i><SPAN class="Yellow3">in</SPAN></i>
         <SPAN class="Grey2">compose</SPAN> <SPAN class="Grey2">ss</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Grey2">s1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
      <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3">exception</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">unify</SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
       <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Blue1">false</SPAN></SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">vn</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>  
                        <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">vn</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">v</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2"><SPAN class="Blue1">true</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>  
                        <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">s</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">orelse</SPAN></SPAN></i> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">vn</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">vn</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">v</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Brown1">rev</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Arity</SPAN><SPAN class="Blue1">&quot;</SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Arity</SPAN><SPAN class="Blue1">&quot;</SPAN>
          <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t1s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t2</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t2s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
               <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">compose</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> 
                                            <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t1s</SPAN> <SPAN class="Grey2">t2s</SPAN>
    <i><SPAN class="Yellow3">in</SPAN></i>  
       <i><SPAN class="Yellow3"><SPAN class="Blue2">case</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i>
          <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">v2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">v2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
             <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">t2</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Occurs</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
             <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">occurs</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">t1</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Occurs</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
                <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name1</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">name2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> 
                   <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">unify_args</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">args1</SPAN> <SPAN class="Grey2">args2</SPAN> 
                   <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Const</SPAN><SPAN class="Blue1">&quot;</SPAN>
    <i><SPAN class="Yellow3">end</SPAN></i>
<i><SPAN class="Yellow3">in</SPAN></i>
   <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN>
<i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3">datatype</SPAN></i> <SPAN class="Grey2">typescheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Forall</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Grey2">typescheme</SPAN>
                    <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">Type</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">term</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mem</SPAN> <SPAN class="Grey2">p</SPAN> <SPAN class="Grey2">l</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Blue1">false</SPAN></SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">xs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">orelse</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">xs</SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">l</SPAN> <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">mem</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
      <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
            <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Grey2">t</SPAN> 
                <i><SPAN class="Yellow3">in</SPAN></i> 
                   <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">ts</SPAN> 
                <i><SPAN class="Yellow3">end</SPAN></i>
      <i><SPAN class="Yellow3">in</SPAN></i>
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">fvs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">args</SPAN> <i><SPAN class="Yellow3">in</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3">end</SPAN></i>
      <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">s</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">b</SPAN> <SPAN class="Grey2">t</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">tyvars</SPAN> <SPAN class="Grey2">t</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">t</SPAN> <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">f</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">b</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">varno</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Green3">~</SPAN><SPAN class="Green3">1</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">varno</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
    <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">vl</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">explode</SPAN> <SPAN class="Grey2">v</SPAN>
        <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">letter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ord</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2"><SPAN class="Brown1">hd</SPAN></SPAN> <SPAN class="Grey2">vl</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3"><SPAN class="Green3">-</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ord</SPAN> <SPAN class="Purple3">#</SPAN><SPAN class="Purple3">&quot;</SPAN><SPAN class="Blue2">a</SPAN><SPAN class="Purple3">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
        <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">primes</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">primes</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
              <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">h</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Purple3">#</SPAN><SPAN class="Purple3">&quot;</SPAN><SPAN class="Blue1">\</SPAN><SPAN class="Red1">039</SPAN><SPAN class="Purple3">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">primes</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Grey3"><SPAN class="Green3">+</SPAN></SPAN><SPAN class="Green3">26</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Green3">~</SPAN><SPAN class="Green3">1</SPAN>
    <i><SPAN class="Yellow3">in</SPAN></i> 
       <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">letter</SPAN> <SPAN class="Grey3"><SPAN class="Green3">&gt;=</SPAN></SPAN> <SPAN class="Green3">0</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">andalso</SPAN></SPAN></i> <SPAN class="Grey2">letter</SPAN> <SPAN class="Grey3"><SPAN class="Green3">&lt;=</SPAN></SPAN> <SPAN class="Green3">25</SPAN> 
          <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">primes</SPAN> <SPAN class="Grey2">letter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2"><SPAN class="Brown1">tl</SPAN></SPAN> <SPAN class="Grey2">vl</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Green3">~</SPAN><SPAN class="Green3">1</SPAN>
    <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">lastusedtsvar</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">sigma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">vars</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">b</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN> <i><SPAN class="Yellow3">in</SPAN></i> <SPAN class="Grey2">f</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">b</SPAN> <i><SPAN class="Yellow3">end</SPAN></i>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
               <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">vn</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">varno</SPAN> <SPAN class="Grey2">h</SPAN> <i><SPAN class="Yellow3">in</SPAN></i> 
                  <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">vn</SPAN> <SPAN class="Grey3"><SPAN class="Green3">&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">vn</SPAN> <SPAN class="Grey2">t</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">t</SPAN> 
               <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">vars</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">lastfreetsvar</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">sigma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">vars</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
               <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">vn</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">varno</SPAN> <SPAN class="Grey2">h</SPAN> <i><SPAN class="Yellow3">in</SPAN></i> 
                  <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">vn</SPAN> <SPAN class="Grey3"><SPAN class="Green3">&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">vn</SPAN> <SPAN class="Grey2">t</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">t</SPAN> 
               <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">vars</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">newvar</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Grey3"><SPAN class="Green3">+</SPAN></SPAN><SPAN class="Green3">1</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">prime</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Green3">0</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">prime</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">n</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">prime</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">'</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN><SPAN class="Grey3"><SPAN class="Green3">-</SPAN></SPAN><SPAN class="Green3">1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">primes</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2"><SPAN class="Green3">div</SPAN></SPAN> <SPAN class="Green3">26</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">var</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">str</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">chr</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ord</SPAN> <SPAN class="Purple3">#</SPAN><SPAN class="Purple3">&quot;</SPAN><SPAN class="Blue2">a</SPAN><SPAN class="Purple3">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3"><SPAN class="Green3">+</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2"><SPAN class="Green3">mod</SPAN></SPAN> <SPAN class="Green3">26</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">prime</SPAN> <SPAN class="Grey2">var</SPAN> <SPAN class="Grey2">primes</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">tssubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">tssubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">tvp</SPAN> <i><SPAN class="Yellow3">as</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">tvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
     <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">t</SPAN>
         <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">rnss</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">tvp</SPAN> <i><SPAN class="Yellow3">as</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ts</SPAN> <i><SPAN class="Yellow3">as</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">sv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
           <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">sv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i>
              <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">mem</SPAN> <SPAN class="Grey2">sv</SPAN> <SPAN class="Grey2">fvs</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> 
                  <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">newv</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">newvar</SPAN> <SPAN class="Grey2">nv</SPAN>
                      <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                        <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">compose</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">newv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sv</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">rnss</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">tvp</SPAN> <SPAN class="Grey2">sts</SPAN>
                  <i><SPAN class="Yellow3">in</SPAN></i> 
                     <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">newv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                  <i><SPAN class="Yellow3">end</SPAN></i> 
              <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">rnss</SPAN> <SPAN class="Grey2">tvp</SPAN> <SPAN class="Grey2">sts</SPAN>
                   <i><SPAN class="Yellow3">in</SPAN></i>
                      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">sv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                   <i><SPAN class="Yellow3">end</SPAN></i>
           <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">rnss</SPAN> <SPAN class="Grey2">tvp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
              <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">tvp</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">rnss</SPAN> <SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">tvp</SPAN> <SPAN class="Grey2">sigma</SPAN>
     <i><SPAN class="Yellow3">in</SPAN></i>
        <SPAN class="Grey2">tssubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">tvs</SPAN> <SPAN class="Grey2">sigma'</SPAN>
     <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3">exception</SPAN></i> <SPAN class="Grey2">Assum</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">assq</SPAN> <SPAN class="Grey2">p</SPAN> <SPAN class="Grey2">l</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Assum</SPAN> <SPAN class="Grey2">p</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">k</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">xs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">k</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">v</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">xs</SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">l</SPAN> <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">fassumvars</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">f</SPAN>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">Gamma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
        <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">ts</SPAN> <i><SPAN class="Yellow3">in</SPAN></i>
           <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">Gamma'</SPAN>
        <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">assumvars</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">f</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">Gamma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
            <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">bvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtsvs</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">ts</SPAN>
            <i><SPAN class="Yellow3">in</SPAN></i>
               <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">fvs</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">bvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">Gamma'</SPAN>
            <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">lastfreeassumvar</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">Gamma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
              <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lastfreetsvar</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">Gamma'</SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Green3">~</SPAN><SPAN class="Green3">1</SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">assumsubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2"><SPAN class="Brown1">rev</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">Gamma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">tssubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Grey2">sigma</SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i>
             <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Grey2">Gamma'</SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">tsclosure</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">tau</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">favs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fassumvars</SPAN> <SPAN class="Grey2">Gamma</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ftvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">fbtyvars</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">tau</SPAN>
       <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">bvs</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">tau</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">bvs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">vs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
              <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">mem</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">favs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">orelse</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">mem</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">bvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> 
                    <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">bvs</SPAN> <SPAN class="Grey2">vs</SPAN> 
                    <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">bvs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">vs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">ftvs</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3">datatype</SPAN></i> <SPAN class="Grey2">exp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN>
             <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">Comb</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">exp</SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Grey2">exp</SPAN>
             <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Grey2">string</SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Grey2">exp</SPAN>
             <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">Let</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">string</SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Grey2">exp</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3"><SPAN class="Green3">*</SPAN></SPAN> <SPAN class="Grey2">exp</SPAN>

<SPAN class="Grey2">infixr</SPAN> <SPAN class="Grey3">--&gt;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">tau1</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">tau2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">%f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau2</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3"><SPAN class="Blue2">case</SPAN></SPAN></i> <SPAN class="Grey2">e</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> 
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">tsinst</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">tau</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">tau</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
               <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">tsinst</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                     <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">newvar</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lastusedtsvar</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                         <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">sigma'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                           <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">tssubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">sigma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                     <i><SPAN class="Yellow3">in</SPAN></i>
                        <SPAN class="Grey2">tsinst</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">sigma'</SPAN>
                     <i><SPAN class="Yellow3">end</SPAN></i>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">tau</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">tsinst</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">assq</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i>
            <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">tau</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
          <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">e1</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">S1Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">assumsubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S1</SPAN> <SPAN class="Grey2">Gamma</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S1Gamma</SPAN> <SPAN class="Grey2">e2</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">S2tau1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">S2</SPAN> <SPAN class="Grey2">tau1</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">newvar</SPAN> <SPAN class="Grey2">nv</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">V</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">unify</SPAN> <SPAN class="Grey2">S2tau1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">tau2</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">Vbeta</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">V</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">VS2S1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">compose</SPAN> <SPAN class="Grey2">V</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">compose</SPAN> <SPAN class="Grey2">S2</SPAN> <SPAN class="Grey2">S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i> 
             <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">VS2S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">Vbeta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>
    <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN>
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">newvar</SPAN> <SPAN class="Grey2">nv</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">S1beta</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">S1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i> 
            <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S1beta</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i> 
    <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Let</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN>
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">e1</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">S1Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">assumsubs</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Grey2">S1</SPAN> <SPAN class="Grey2">Gamma</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                   <SPAN class="Grey2">W</SPAN> <SPAN class="Grey2">nv</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tsclosure</SPAN> <SPAN class="Grey2">S1Gamma</SPAN> <SPAN class="Grey2">tau1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">S1Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e2</SPAN>
             <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">S2S1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">compose</SPAN> <SPAN class="Grey2">S2</SPAN> <SPAN class="Grey2">S1</SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i> 
            <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">nv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S2S1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tau2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">var</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">tau</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">W</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lastfreeassumvar</SPAN> <SPAN class="Grey2">Gamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Grey2">e</SPAN> 
       <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">SGamma</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">assumsubs</SPAN> <SPAN class="Grey2">var</SPAN> <SPAN class="Grey2">S</SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">tsclosure</SPAN> <SPAN class="Grey2">SGamma</SPAN> <SPAN class="Grey2">tau</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">pptsterm</SPAN> <SPAN class="Grey2">tau</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">prec</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">name</SPAN>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">prec</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">name</SPAN>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">prec</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">%f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">a1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">a2</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">maybebracket</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">prec</SPAN> <SPAN class="Grey3"><SPAN class="Green3">&lt;=</SPAN></SPAN> <SPAN class="Green3">10</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Grey2">s</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">(</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">)</SPAN><SPAN class="Blue1">&quot;</SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i>
            <SPAN class="Grey2">maybebracket</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Green3">11</SPAN> <SPAN class="Grey2">a1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2"> -&gt; </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Green3">10</SPAN> <SPAN class="Grey2">a2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>
     <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">prec</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
         <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
               <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                    <SPAN class="Grey2">arglist</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">iter</SPAN> <SPAN class="Green3">30</SPAN> <SPAN class="Grey2">h</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">, </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN>
         <i><SPAN class="Yellow3">in</SPAN></i>  
            <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2"><SPAN class="Brown1">length</SPAN></SPAN> <SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3"><SPAN class="Green3">&gt;</SPAN></SPAN> <SPAN class="Green3">1</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">arglist</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">(</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">) </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">name</SPAN> 
                                 <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">arglist</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2"> </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">name</SPAN>
         <i><SPAN class="Yellow3">end</SPAN></i>
   <i><SPAN class="Yellow3">in</SPAN></i>
       <SPAN class="Grey2">iter</SPAN> <SPAN class="Green3">10</SPAN> <SPAN class="Grey2">tau</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppterm</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">name</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">ppterm</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">name</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">ppterm</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
      <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
            <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">arglist</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">h</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
                 <SPAN class="Grey2">arglist</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppterm</SPAN> <SPAN class="Grey2">h</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">,</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN>
      <i><SPAN class="Yellow3">in</SPAN></i>  
         <SPAN class="Grey2">name</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">arglist</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">(</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">)</SPAN><SPAN class="Blue1">&quot;</SPAN>
      <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppsubs</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">]</SPAN><SPAN class="Blue1">&quot;</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">var</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
               <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppterm</SPAN> <SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">/</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">var</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">,</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN>
    <i><SPAN class="Yellow3">in</SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">[</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">s</SPAN> <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppe</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
      <i><SPAN class="Yellow3"><SPAN class="Blue2">case</SPAN></SPAN></i> <SPAN class="Grey2">e</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">of</SPAN></SPAN></i> 
         <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">v</SPAN>
       <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">(</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2"> </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">)</SPAN><SPAN class="Blue1">&quot;</SPAN> 
       <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">(</SPAN><SPAN class="Blue1">\</SPAN><SPAN class="Red1">\</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">.</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">)</SPAN><SPAN class="Blue1">&quot;</SPAN>
       <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Let</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">let </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">=</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2"> in </SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">ppe</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">e</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">sigma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Forall</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">sv</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">!</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">sv</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">.</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">sts</SPAN>  
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pptsterm</SPAN> <SPAN class="Grey2">term</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">sigma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">ppassums</SPAN> <SPAN class="Grey2">Gamma</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
         <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">assums</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
              <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">:</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">ts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">assums</SPAN><SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">,</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">assums</SPAN>
   <i><SPAN class="Yellow3">in</SPAN></i>
      <SPAN class="Grey2">iter</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">Gamma</SPAN>
   <i><SPAN class="Yellow3">end</SPAN></i>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Examples </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Unification </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">y</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">y</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">z</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">z</SPAN><SPAN class="Blue1">&quot;</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">apply</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Grey2">l</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">l</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">a</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">apply</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">a</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">j</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">apply</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">j</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">apply</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">t1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">j</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">t2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">j</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">a</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">a</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppterm</SPAN> <SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppterm</SPAN> <SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">U</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">unify</SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppsubs</SPAN> <SPAN class="Grey2">U</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">print</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppterm</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">U</SPAN> <SPAN class="Grey2">t1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">\</SPAN><SPAN class="Red1">n</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">print</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ppterm</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">subs</SPAN> <SPAN class="Grey2">U</SPAN> <SPAN class="Grey2">t2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Blue1"><SPAN class="Grey3">^</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Blue1">\</SPAN><SPAN class="Red1">n</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Constructors for types </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_func</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Grey2">args</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyapp</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">name</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">args</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_nullary</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_func</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_unary</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Grey2">arg</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_func</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">arg</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_binary</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Grey2">arg1</SPAN> <SPAN class="Grey2">arg2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_func</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">arg1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">arg2</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_ternary</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Grey2">arg1</SPAN> <SPAN class="Grey2">arg2</SPAN> <SPAN class="Grey2">arg3</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_func</SPAN> <SPAN class="Grey2">name</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">arg1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">arg2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">arg3</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">pairt</SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_binary</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">pair</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">t1</SPAN> <SPAN class="Grey2">t2</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">t</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_unary</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">list</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">t</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">boolt</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_nullary</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">bool</SPAN><SPAN class="Blue1">&quot;</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Type variables </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">a</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">beta</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">b</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">alpha'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">a'</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">beta'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">b'</SPAN><SPAN class="Blue1">&quot;</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Type-schemes </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">t</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Type</SPAN> <SPAN class="Grey2">t</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Tyvar</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">vs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">t</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Forall</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Grey2">vs</SPAN> <SPAN class="Grey2">t</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Fail</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">mk_tyscheme: Invalid type-scheme.</SPAN><SPAN class="Blue1">&quot;</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Now we can construct type-schemes. For example here is a</i></SPAN>
<SPAN class="Green3"><i>   polymorphic function taking pairs of functions and two lists to a</i></SPAN>
<SPAN class="Green3"><i>   list of pairs: </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">dmapts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">alpha'</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta'</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> 
                  <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pairt</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">beta</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">beta'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> 
                      <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">beta</SPAN>
                      <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">pairt</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">beta'</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">dmapts</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Lambda expressions with let bindings </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">labs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">labs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Fail</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">labs: Invalid argument</SPAN><SPAN class="Blue1">&quot;</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">llet</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e1</SPAN> <SPAN class="Grey2">e2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Let</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">llet</SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">_</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">Fail</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">llet: Invalid argument</SPAN><SPAN class="Blue1">&quot;</SPAN>

<SPAN class="Grey2">infix</SPAN> <SPAN class="Grey3">@:</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">e1</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">e2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e2</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">e</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">xs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">labs</SPAN> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Grey2">xs</SPAN> <SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">letbind</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">e</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">letbind</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">v</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">e1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">bs</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">e</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">llet</SPAN> <SPAN class="Grey2">v</SPAN> <SPAN class="Grey2">e1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">letbind</SPAN> <SPAN class="Grey2">bs</SPAN> <SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">lapply</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
  <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">lapply</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">e</SPAN><SPAN class="Grey3"><SPAN class="Brown1">::</SPAN></SPAN><SPAN class="Grey2">es</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lapply</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">e</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey2">es</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Variables </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">y</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">y</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">z</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">z</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">p</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">p</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">m</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">m</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">n</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">n</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">s</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">i</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">i</SPAN><SPAN class="Blue1">&quot;</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Church numerals </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">num</SPAN> <SPAN class="Grey2">n</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
  <i><SPAN class="Yellow3">let</SPAN></i> <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN>
      <i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN>
      <i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Green3">0</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">r</SPAN>
        <SPAN class="Red3"><SPAN class="Brown2">|</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">r</SPAN> <SPAN class="Grey2">n</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">iter</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN><SPAN class="Grey3"><SPAN class="Green3">-</SPAN></SPAN><SPAN class="Green3">1</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
  <i><SPAN class="Yellow3">in</SPAN></i>
     <SPAN class="Grey2">iter</SPAN> <SPAN class="Grey2">x</SPAN> <SPAN class="Grey2">n</SPAN>
  <i><SPAN class="Yellow3">end</SPAN></i>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Now we can construct assumptions and expressions </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> S ZERO = </i></SPAN><SPAN class="Green3"><i>(λ n f x.n f </i></SPAN><SPAN class="Green3"><i>(f x)) λ f x.x  </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">ZERO</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">num</SPAN> <SPAN class="Green3">0</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">S</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">n</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">S</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">ZERO</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> PRED and PRED 6 </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">PAIR</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">x</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">FST</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">p</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">SND</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">p</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">G</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">PAIR</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">FST</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">FST</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">p</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">PRED</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">n</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">SND</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">G</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">S</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">PAIR</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">ZERO</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">ZERO</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">SUB</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">m</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">n</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">PRED</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">m</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">PRED</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">PRED</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">num</SPAN> <SPAN class="Green3">6</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">SUB</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> The definition of PRED from Larry Paulson's lecture notes </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">PREDp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">n</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">SND</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">G</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">PAIR</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">x</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">SUBp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">m</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">n</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">n</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">PREDp</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">m</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">PREDp</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">PREDp</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">num</SPAN> <SPAN class="Green3">6</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">SUBp</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">SUBp</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> let i=λx.x in i i </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">polylet</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">letbind</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">i</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">i</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">i</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">polylet</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">polylet</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> map </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">condts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">boolt</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">fixts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">nullts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">boolt</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">nilts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">consts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">hdts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">tlts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">listt</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">pairts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">beta</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">pairt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">fstts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pairt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey2">beta</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">sndts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">mk_tyscheme</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">alpha</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pairt</SPAN> <SPAN class="Grey2">alpha</SPAN> <SPAN class="Grey2">beta</SPAN> <SPAN class="Grey3">--&gt;</SPAN> <SPAN class="Grey2">beta</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">bool_assums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">true</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Type</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">boolt</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">false</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Type</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">boolt</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">cond</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">condts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">pair_assums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">pair</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">pairts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">fst</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">fstts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">snd</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">sndts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">fix_assums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">fix</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">fixts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">list_assums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">null</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">nullts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">nil</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">nilts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
                   <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">cons</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">consts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">hd</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">hdts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">tl</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">tlts</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> let map = </i></SPAN><SPAN class="Green3"><i>(fix </i></SPAN><SPAN class="Green3"><i>(λ map f s.</i></SPAN>
<SPAN class="Green3"><i>                 </i></SPAN><SPAN class="Green3"><i>(cond </i></SPAN><SPAN class="Green3"><i>(null s) nil</i></SPAN>
<SPAN class="Green3"><i>                       </i></SPAN><SPAN class="Green3"><i>(cons </i></SPAN><SPAN class="Green3"><i>(f </i></SPAN><SPAN class="Green3"><i>(hd s)) </i></SPAN><SPAN class="Green3"><i>(map f </i></SPAN><SPAN class="Green3"><i>(tl s)))))) in map </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">assums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">bool_assums</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">fix_assums</SPAN><SPAN class="Grey3"><SPAN class="Brown1">@</SPAN></SPAN><SPAN class="Grey2">list_assums</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">map'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">map</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">fix</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">fix</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">null'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">null</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">nil'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">nil</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cond</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">cond</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cons</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">cons</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">hd'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">hd</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">tl'</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">tl</SPAN><SPAN class="Blue1">&quot;</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">mapdef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
   <SPAN class="Grey2">letbind</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">map'</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
           <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">fix</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">map'</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">f</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> 
                         <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">cond</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">null'</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                               <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">nil'</SPAN> 
                               <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">cons</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">hd'</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
                                       <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">map'</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">tl'</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">s</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> 
            <SPAN class="Grey2">map'</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppassums</SPAN> <SPAN class="Grey2">assums</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">mapdef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">mapdefts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Grey2">assums</SPAN> <SPAN class="Grey2">mapdef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">mapdefts</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Mairson's expression in ML</i></SPAN>
<SPAN class="Green3"><i>let fun pair x y = fn z =&gt; z x y </i></SPAN>
<SPAN class="Green3"><i>    val x1 = fn y =&gt; pair y y </i></SPAN>
<SPAN class="Green3"><i>    val x2 = fn y =&gt; x1 </i></SPAN><SPAN class="Green3"><i>(x1 y)</i></SPAN>
<SPAN class="Green3"><i>    val x3 = fn y =&gt; x2 </i></SPAN><SPAN class="Green3"><i>(x2 y)</i></SPAN>
<SPAN class="Green3"><i>    val x4 = fn y =&gt; x3 </i></SPAN><SPAN class="Green3"><i>(x3 y)</i></SPAN>
<SPAN class="Green3"><i>    val x5 = fn y =&gt; x4 </i></SPAN><SPAN class="Green3"><i>(x4 y)</i></SPAN>
<SPAN class="Green3"><i>in</i></SPAN>
<SPAN class="Green3"><i>   x5 </i></SPAN><SPAN class="Green3"><i>(fn z =&gt; z)</i></SPAN>
<SPAN class="Green3"><i>end</i></SPAN>
<SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x1</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x1</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x2</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x2</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x3</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x3</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x4</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x4</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">x5</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x5</SPAN><SPAN class="Blue1">&quot;</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">pair</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">pair</SPAN><SPAN class="Blue1">&quot;</SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">mairson</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> 
   <SPAN class="Grey2">letbind</SPAN> 
     <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pair</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">z</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">z</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">x</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x1</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">pair</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x2</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x1</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x1</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x3</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x2</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x2</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN>
      <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x4</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x3</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x3</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Grey2">y</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
 <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">x4</SPAN> <SPAN class="Grey3">@:</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">lambda</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppts</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">mairson</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN>
<SPAN class="Green3"><i>val mairson = </i></SPAN>
<SPAN class="Green3"><i>   letbind </i></SPAN>
<SPAN class="Green3"><i>     [</i></SPAN><SPAN class="Green3"><i>(pair,lambda [x,y,z] </i></SPAN><SPAN class="Green3"><i>(z @: x @: y)),</i></SPAN>
<SPAN class="Green3"><i>      </i></SPAN><SPAN class="Green3"><i>(x1,lambda [y] </i></SPAN><SPAN class="Green3"><i>(pair @: y @: y)),</i></SPAN>
<SPAN class="Green3"><i>      </i></SPAN><SPAN class="Green3"><i>(x2,lambda [y] </i></SPAN><SPAN class="Green3"><i>(x1 @: </i></SPAN><SPAN class="Green3"><i>(x1 @: y))),</i></SPAN>
<SPAN class="Green3"><i>      </i></SPAN><SPAN class="Green3"><i>(x3,lambda [y] </i></SPAN><SPAN class="Green3"><i>(x2 @: </i></SPAN><SPAN class="Green3"><i>(x2 @: y))),</i></SPAN>
<SPAN class="Green3"><i>      </i></SPAN><SPAN class="Green3"><i>(x4,lambda [y] </i></SPAN><SPAN class="Green3"><i>(x3 @: </i></SPAN><SPAN class="Green3"><i>(x3 @: y))),</i></SPAN>
<SPAN class="Green3"><i>      </i></SPAN><SPAN class="Green3"><i>(x5,lambda [y] </i></SPAN><SPAN class="Green3"><i>(x4 @: </i></SPAN><SPAN class="Green3"><i>(x4 @: y)))</i></SPAN>
<SPAN class="Green3"><i> ] </i></SPAN><SPAN class="Green3"><i>(x5 @: </i></SPAN><SPAN class="Green3"><i>(lambda [x] x));</i></SPAN>

<SPAN class="Green3"><i>principalts [] mairson;</i></SPAN>
<SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> handle expected exceptions </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3">exception</SPAN></i> <SPAN class="Grey2">TestFail</SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">fun</SPAN></SPAN></i> <SPAN class="Grey2">expect_Unify</SPAN> <SPAN class="Grey2">se</SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN>
   <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">ignore</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3">handle</SPAN></i> <SPAN class="Grey2">Unify</SPAN> <SPAN class="Grey2">s</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue3">if</SPAN></SPAN></i> <SPAN class="Grey2">se</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">s</SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">then</SPAN></SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <i><SPAN class="Yellow3"><SPAN class="Blue2">else</SPAN></SPAN></i> <i><SPAN class="Yellow3">raise</SPAN></i> <SPAN class="Grey2">TestFail</SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> omega </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">omegaexp</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Let</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">omega</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">omega</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">omegadef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> 
    <SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">omegaexp</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">expect_Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Occurs</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">omegadef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Y </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">r</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">ydef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Let</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Y</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">r</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Y</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">expect_Unify</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">Occurs</SPAN><SPAN class="Blue1">&quot;</SPAN> <SPAN class="Grey2">ydef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Church numerals </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">nassums</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_zerodef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppassums</SPAN> <SPAN class="Grey2">nassums</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">cn_zerodef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_zero</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">cn_zerodef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_zero</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_onedef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN> <SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppassums</SPAN> <SPAN class="Grey2">nassums</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">cn_onedef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_one</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">cn_onedef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_one</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_twodef</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Abs</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Comb</SPAN><SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">f</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">,</SPAN></SPAN><SPAN class="Grey2">Var</SPAN> <SPAN class="Blue1">&quot;</SPAN><SPAN class="Purple2">x</SPAN><SPAN class="Blue1">&quot;</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppassums</SPAN> <SPAN class="Grey2">nassums</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppexp</SPAN> <SPAN class="Grey2">cn_twodef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3"><SPAN class="Purple2">val</SPAN></SPAN></i> <SPAN class="Grey2">cn_two</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=</SPAN></SPAN> <SPAN class="Grey2">principalts</SPAN> <SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">[</SPAN></SPAN></SPAN><SPAN class="Red3"><SPAN class="Brown2"><SPAN class="Brown1">]</SPAN></SPAN></SPAN> <SPAN class="Grey2">cn_twodef</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_two</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_zero</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_one</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<SPAN class="Grey2">ppts</SPAN> <SPAN class="Grey2">cn_two</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>

<SPAN class="Green3"><i>(</i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i> Church numerals in SML </i></SPAN><SPAN class="Red2">*</SPAN><SPAN class="Green3"><i>)</i></SPAN>

<i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">;</SPAN></SPAN>
<i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <i><SPAN class="Yellow3">fn</SPAN></i> <SPAN class="Grey2">x</SPAN> <SPAN class="Red3"><SPAN class="Brown2">=&gt;</SPAN></SPAN> <SPAN class="Grey2">f</SPAN> <SPAN class="Red3"><SPAN class="Brown2">(</SPAN></SPAN><SPAN class="Grey2">f</SPAN> <SPAN class="Grey2">x</SPAN><SPAN class="Red3"><SPAN class="Brown2">)</SPAN></SPAN>

</PRE></BODY>
